/* Copyright (C) 2013-2021 TU Dortmund
 * This file is part of LearnLib, http://www.learnlib.de/.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package de.learnlib.examples;

import de.learnlib.algorithms.discriminationtree.mealy.DTLearnerMealy;
import de.learnlib.algorithms.discriminationtree.mealy.DTLearnerMealyBuilder;
import de.learnlib.api.oracle.MembershipOracle.MealyMembershipOracle;
import de.learnlib.api.query.DefaultQuery;
import de.learnlib.counterexamples.LocalSuffixFinders;
import de.learnlib.filter.cache.mealy.MealyCacheOracle;
import de.learnlib.filter.cache.mealy.MealyCaches;
import de.learnlib.filter.statistic.oracle.MealyCounterOracle;
import de.learnlib.oracle.equivalence.MealyWpMethodEQOracle;
import de.learnlib.oracle.membership.SimulatorOracle.MealySimulatorOracle;
import net.automatalib.automata.transducers.MealyMachine;
import net.automatalib.automata.transducers.impl.compact.CompactMealy;
import net.automatalib.util.automata.Automata;
import net.automatalib.util.automata.random.RandomAutomata;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.Alphabets;

import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.*;

/**
 * This example shows the usage of a learning algorithm and an equivalence test as part of an experiment in order to
 * learn a simulated SUL (system under learning).
 *
 * @author falkhowar
 */
@SuppressWarnings("PMD.SystemPrintln")
public final class Example4 {

    private static final int EXPLORATION_DEPTH = 4;

    private Example4() {
        // prevent instantiation
    }

    public static void main(String[] args) throws IOException {

        // load Mealy and alphabet
        final int sizeInput = 10;
        final int sizeOutput = 10;
        final int size = 100;

        CompactMealy<Integer,Integer> model = constructSUL(sizeInput,sizeOutput,size);

        Alphabet<Integer> alphabet = model.getInputAlphabet();
        // construct a simulator membership query oracle
        // input  - I (determined by example)
        MealyMembershipOracle<Integer,Integer> sul = new MealySimulatorOracle<>(model);
        // oracle for counting queries wraps SUL
        MealyCounterOracle<Integer,Integer> mqOracle = new MealyCounterOracle<>(sul, "membership queries");
        MealyCacheOracle<Integer,Integer> CacheOracle = MealyCaches.createTreeCache(alphabet, mqOracle);

        // construct L* instance
        DTLearnerMealy<Integer,Integer> learner = new DTLearnerMealyBuilder<Integer,Integer>().withAlphabet(alphabet) // input alphabet
                .withOracle(CacheOracle) // membership oracle
                .withSuffixFinder(LocalSuffixFinders.RIVEST_SCHAPIRE)
                .create();
       /*ExtensibleLStarMealy<Integer,Integer> learner = new ExtensibleLStarMealyBuilder<Integer,Integer>()
                .withAlphabet(alphabet).withOracle(CacheOracle)
                .withCexHandler(ObservationTableCEXHandlers.CLASSIC_LSTAR).withClosingStrategy(ClosingStrategies.CLOSE_FIRST)
                .withInitialSuffixes(Collections.emptyList())
                .create();
        /*ClassicLStarMealy<Integer,Integer> learner = new ClassicLStarMealyBuilder<Integer,Integer>()
                .withAlphabet(alphabet).withOracle(sul)
                .withCexHandler(ObservationTableCEXHandlers.CLASSIC_LSTAR).withClosingStrategy(ClosingStrategies.CLOSE_FIRST)
                .withInitialSuffixes(Collections.emptyList())
                .create();
        /*ShahbazMealy<Integer> lstar =
                new ShahbazMealyBuilder<Integer>().withAlphabet(inputs) // input alphabet
                .withOracle(CacheOracle) // membership oracle
                .create();
        /*DTLearnerMealy<Integer> lstar=
                new DTLearnerMealyBuilder<Integer>().withAlphabet(inputs) // input alphabet
                .withOracle(CacheOracle) // membership oracle
                .withSuffixFinder(LocalSuffixFinders.RIVEST_SCHAPIRE)
                .create();
        /*RivestSchapireMealy<Integer> lstar = new RivestSchapireMealyBuilder<I>().withAlphabet(inputs) // input alphabet
                .withOracle(CacheOracle) // membership oracle
                .create();*/
        // construct a W-method conformance test
        // exploring the system up to depth 4 from
        // every state of a hypothesis
        MealyWpMethodEQOracle<Integer,Integer> wMethod = new MealyWpMethodEQOracle<>(CacheOracle,0,100);
        //MealyRandomWMethodEQOracle<I> wMethod = new MealyRandomWMethodEQOracle<>(CacheOracle, 0,6);
        //MealyRandomWordsEQOracle<I> wMethod = new MealyRandomWordsEQOracle<>(CacheOracle, 0,10,200);
        // construct a learning experiment from
        // the learning algorithm and the conformance test.
        // The experiment will execute the main loop of
        // active learning
        learner.startLearning();

        final MealyMachine<?,Integer,?,Integer> hyp = learner.getHypothesisModel();
        long rounds = 0L;
        while (true) {
            if(Automata.findSeparatingWord(model, hyp, alphabet) == null )
                break;
            System.out.println("Searching for counterexample");

            DefaultQuery<Integer, Word<Integer>> ce = wMethod.findCounterExample(hyp, alphabet);

            if (ce == null) {
                break;
            }

            System.out.println(ce.getInput().toString());

            // next round ...
            rounds++;
            System.out.println("Starting round " + rounds);
            System.out.println("Learning");

            final boolean refined = learner.refineHypothesis(ce);
            assert refined;
        }


        MealyMachine<?,Integer,?,Integer> result = learner.getHypothesisModel();
        System.out.println("States: " + result.size());
        System.out.println("Sigma: " + alphabet.size());


        System.out.println(rounds);
        System.out.println(mqOracle.getCount());
        System.out.println(mqOracle.getSymbolCount());
        if(Automata.findSeparatingWord(model, result, alphabet) == null )
            System.out.println("Learning algorithm is correct");
        System.out.println("Model: ");


       // new ObservationTableASCIIWriter<>().write(learner.getObservationTable(), System.out);
        /*
        GraphDOT.write(result, alphabet, System.out); // may throw IOException!

        Visualization.visualize(result, alphabet);

        System.out.println("-------------------------------------------------------");

        System.out.println("Final observation table:");

        */
        //OTUtils.displayHTMLInBrowser(learner.getObservationTable());
    }

    /**
     * creates random mealy
     *
     * @return a mealy
     */
    private static CompactMealy<Integer,Integer> constructSUL(int numInputs,int numOutputs, int size) {
        CompactMealy<Integer,Integer> randomMealy = RandomAutomata.randomMealy(new Random(), size, Alphabets.integers(0, numInputs - 1), Alphabets.integers(0, numOutputs - 1));
       //Visualization.visualize(randomDfa, Alphabets.integers(0, numInputs - 1));
        return randomMealy;
    }

    private static void recordSUL( CompactMealy<Integer,Integer> randomMealy, int size,int index) {
        try {
            PrintWriter out = new PrintWriter("/home/pany/model/learnlib/algorithms/active/ttt/src/test/resources/Mealy"+size+"-"+randomMealy.getInputAlphabet().size()+"-10_"+index+".mealy");//输出的路径和文件名

            out.printf("%d %d %n", randomMealy.size(), randomMealy.getInputAlphabet().size());

            for (int i = 0; i < randomMealy.size(); i++) {
                for (int j = 0; j < randomMealy.getInputAlphabet().size(); j++)
                {
                    out.printf("%d ", randomMealy.getSuccessor(i, j));
                }
                out.printf("%n");
            }

            for (int i = 0; i < randomMealy.size(); i++) {
                for (int j = 0; j < randomMealy.getInputAlphabet().size(); j++)
                {
                    out.printf("%d ", randomMealy.getOutput(i,j)) ;
                }
                out.printf("%n");
            }
            out.close();
        } catch (FileNotFoundException e) {
            throw new RuntimeException(e);
        }
    }

}
